#include "cuddObj.hh"

int main(int argc, char* argv[]) {

  Cudd *mgr = new Cudd(0,0);

  int verbosity = 2;
  cout << "Entering testBdd\n";
  // Create two new variables in the manager. If testBdd is called before
  // any variable is created in mgr, then x gets index 0 and y gets index 1.
  BDD x = mgr->bddVar();
  BDD y = mgr->bddVar();
  
  BDD f = x * y;
  cout << "f"; f.print(2,verbosity);
  
  BDD g = y * !x;
  cout << "g"; g.print(2,verbosity);
  
  cout << "f and g are" << (f == !g ? "" : " not") << " complementary\n";
  cout << "f is" << (f <= g ? "" : " not") << " less than or equal to  g\n";
  cout << "g is" << (g <= f ? "" : " not") << " less than or equal to f\n";
  
  g = f | ~g;
  cout << "g"; g.print(2,verbosity);
  
  BDD h = f = y;
  cout << "h"; h.print(2,verbosity);
  
  cout << "x + h has " << (x+h).nodeCount() << " nodes\n";
  
  h += x;
  cout << "h"; h.print(2,verbosity);
}
